cluster predicate - unidirectional graph reachability matrix

Questions/notes:
1. Is there an autoformatter?
2. I'm not sure about the `multiroot` suffix, should it be `anyroot`?
3. Also, is `cluster` the best name? Is `constellations`/`sccs` better?

I needed this some time back, and having this
would have saved me quite some time.

Essentially, this ended up consisting of two parts:
1. `reachable_multiroot()` - a seemingly rather boringly straight-forward
    generalization of the `reachable()`, which, instead of enforcing that
    the subgraph is reachable from _the_ root node (given by index,
    non-optional), and thus forcing there to be a single joint subgraph,
    instead takes (zero or more) roots as a mask.
    The rest of the logic is generalized accordingly.
2. `cluster()` predicate.
    This one took **_quite_** a bit of rewrites to fully distill it
    to it's purest+simplest+fastest form. :) The (final) basic idea is to,
    basically, give each node a unique "color", and then set the nodes,
    linked together by selected edges, to the same color,
    thus ensuring that the nodes, that are not in any way connected,
    don't have the same "color", and vice versa.

    Implementation-wise, instead of color, for each node, we track the index of
    the disjoint subgraph to which this node belongs, and it turned out
    that tracking that by tracking the root node of each subgraph is
    the best approach (referred to as root). So there's 3 parts:
    1. Splitting disjoint subgraphs: we then defer to `reachable_multiroot()`
       to enfore that each disjoint subgraph actually has a root node,
       thus different disjoint subgraphs have different roots.
    2. Coalescing same-color subgraphs: nodes, that are linked together
       by selected edge, have the same root.
    3. And then we actually compute reachability matrix based on whether or not
       two nodes have same root (belong to the same disjoint subgraph)

    **Now, this is controversial. I've decided to return the reachability
    matrix, *NOT* the subgraph index. While sparse data structure seems better,
    it immediately requires symmetry breaking constraint, which is tricky
    (i have written it.), and `--all-solutions` actually ends up being *MUCH*
    slower (`O^3`?) than just returning reachability matrix...
    The directed version would need to return the matrix,
    so this is also future-proofing for consistency sake**

I have an exhaustive test harness for the `cluster()` (but not the rest),
it would not have been possible to refine the predicate so much otherwise,
please see https://github.com/LebedevRI/minizinc-graph-reachability-matrix-predicate.mzn/tree/proof-of-concept/unidirectional

Author: LebedevRI

share/minizinc/std/cluster.mzn

@@ -0,0 +1,56 @@
+include "fzn_cluster_int.mzn";
+include "fzn_cluster_int_reif.mzn";
+include "fzn_cluster_enum.mzn";
+include "fzn_cluster_enum_reif.mzn";
+
+/** @group globals.graph
+    Clusterize the subgraph \a ns and \a es of a given undirected graph into disjoint subgraphs,
+    and produce a \a r node reachability matrix.
+
+    @param N: the number of nodes in the given graph
+    @param E: the number of edges in the given graph
+    @param from: the leaving node 1..\a N for each edge
+    @param to: the entering node 1..\a N for each edge
+    @param r: node reachability matrix
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate cluster(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                  array[int,int] of var bool: r,
+                  array[int] of var bool: ns, array[int] of var bool: es) =
+    assert(index_set(from) = 1..E,"cluster: index set of from must be 1..\(E)") /\
+    assert(index_set(to) = 1..E,"cluster: index set of to must be 1..\(E)") /\
+    assert(index_set(ns) = 1..N,"cluster: index set of ns must be 1..\(N)") /\
+    assert(index_set(es) = 1..E,"cluster: index set of es must be 1..\(E)") /\
+    fzn_cluster(N,E,from,to,r,ns,es);
+
+/** @group globals.graph
+    Clusterize the subgraph \a ns and \a es of a given undirected graph into disjoint subgraphs,
+    and produce a \a r node reachability matrix.
+
+    @param from: the leaving node for each edge
+    @param to: the entering node for each edge
+    @param r: node reachability matrix
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate cluster(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                  array[$$N,$$N] of var bool: r,
+                  array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        int: NUM_NODES = card(index_set(ns));
+    } in
+    assert(index_set(from) = index_set(to),"cluster: index set of from and to must be identical") /\
+    assert(index_set(from) = index_set(es),"cluster: index set of from and es must be identical") /\
+    assert(index_set_1of2(r) = index_set_2of2(r),"cluster: nodes in from must be in index set of r") /\
+    assert(dom_array(from) subset index_set_1of2(r),"cluster: nodes in from must be in index set of r") /\
+    assert(dom_array(to) subset index_set_1of2(r),"cluster: nodes in to must be in index set of r") /\
+    assert(dom_array(from) subset index_set(ns),"cluster: nodes in from must be in index set of ns") /\
+    assert(dom_array(to) subset index_set(ns),"cluster: nodes in to must be in index set of ns") /\
+    fzn_cluster(
+        index2int(enum2int(from)),
+        index2int(enum2int(to)),
+        index2int(r),
+        index2int(ns),
+        index2int(es)
+    );

share/minizinc/std/fzn_cluster_enum.mzn

@@ -0,0 +1,31 @@
+include "reachable_multiroot.mzn";
+
+predicate fzn_cluster(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                      array[$$N,$$N] of var bool: r,
+                      array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        array[index_set(ns)] of var index_set(ns): NodeRoot;
+        array[index_set(ns)] of var bool: NodeRootnessMask;
+        array[index_set(ns)] of bool: ALL_GRAPH_NODES = [ true | n in index_set(ns) ];
+    } in
+        symmetry_breaking_constraint(forall (j,i in index_set(ns) where i > j)(
+            r[i,j] == r[j,i]
+        )) /\
+        forall (c in index_set(ns))(
+            r[c,c] == true
+        ) /\
+        forall (j,i in index_set(ns) where i > j)(
+            r[j,i] -> (ns[j] /\ ns[i])
+        ) /\
+        reachable_multiroot(from,to,NodeRootnessMask,ALL_GRAPH_NODES,es) /\
+        forall (n in index_set(ns))(
+            NodeRootnessMask[n] == (NodeRoot[n] == n)
+        ) /\
+        forall (e in index_set(es))(
+            es[e] -> (NodeRoot[from[e]] == NodeRoot[to[e]])
+        ) /\
+        forall (j,i in index_set(ns) where i > j)(
+            r[j,i] == (NodeRoot[i] == NodeRoot[j])
+        );
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_cluster_enum_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_cluster_reif(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                           array[$$N,$$N] of var bool: r, array[$$N] of var bool: ns,
+                           array[$$E] of var bool: es, var bool: b) =
+  abort("Reified cluster constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_cluster_int.mzn

@@ -0,0 +1,30 @@
+include "reachable_multiroot.mzn";
+
+predicate fzn_cluster(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                      array[int,int] of var bool: r, array[int] of var bool: ns, array[int] of var bool: es) =
+    let {
+        array[1..N] of var 1..N: NodeRoot;
+        array[1..N] of var bool: NodeRootnessMask;
+        array[1..N] of bool: ALL_GRAPH_NODES = [ true | n in 1..N ];
+    } in
+        symmetry_breaking_constraint(forall (j,i in 1..N where i > j)(
+            r[i,j] == r[j,i]
+        )) /\
+        forall (c in 1..N)(
+            r[c,c] == true
+        ) /\
+        forall (j,i in 1..N where i > j)(
+            r[j,i] -> (ns[j] /\ ns[i])
+        ) /\
+        reachable_multiroot(N,E,from,to,NodeRootnessMask,ALL_GRAPH_NODES,es) /\
+        forall (n in 1..N)(
+            NodeRootnessMask[n] == (NodeRoot[n] == n)
+        ) /\
+        forall (e in 1..E)(
+            es[e] -> (NodeRoot[from[e]] == NodeRoot[to[e]])
+        ) /\
+        forall (j,i in 1..N where i > j)(
+            r[j,i] == (NodeRoot[i] == NodeRoot[j])
+        );
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_cluster_int_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_cluster_reif(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                           array[int,int] of var bool: r, array[int] of var bool: ns,
+                           array[int] of var bool: es, var bool: b) =
+  abort("Reified cluster constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_enum.mzn

@@ -0,0 +1,20 @@
+include "subgraph.mzn";
+
+predicate fzn_dreachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                   array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        array[index_set(ns)] of var 0..card(index_set(ns))-1: dist; /* distance from root */
+        array[index_set(ns)] of var index_set(ns): parent; /* parent */
+    } in
+        forall(n in index_set(ns)) % root nodes must be chosen
+              (rs[n] -> ns[n]) /\
+        forall(n in index_set(ns)) % self-parent is the same as either non-chosen node or root node
+              ((parent[n] = n) == ((not ns[n]) \/ rs[n])) /\
+        forall(n in index_set(ns)) % each non-self-parent node is one more step removed from a root than its parent node
+              (parent[n] != n -> dist[n] = dist[parent[n]] + 1) /\
+        forall(n in index_set(ns)) % each non-self-parent node must have a chosen edge from its parent
+              (parent[n] != n -> exists(e in index_set(from) where to[e] = n)(es[e] /\ from[e] = parent[n])) /\
+        % nodes connected by chosen edges must be chosen
+        subgraph(from,to,ns,es);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_enum_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_dreachable_multiroot_reif(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                        array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es,
+                                        var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_int.mzn

@@ -0,0 +1,20 @@
+include "subgraph.mzn";
+
+predicate fzn_dreachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                   array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    let {
+        array[1..N] of var 0..N-1: dist; /* distance from root */
+        array[1..N] of var 1..N: parent; /* parent */
+    } in
+        forall(n in 1..N) % root nodes must be chosen
+              (rs[n] -> ns[n]) /\
+        forall(n in 1..N) % self-parent is the same as either non-chosen node or root node
+              ((parent[n] = n) == ((not ns[n]) \/ rs[n])) /\
+        forall(n in 1..N) % each non-self-parent node is one more step removed from a root than its parent node
+              (parent[n] != n -> dist[n] = dist[parent[n]] + 1) /\
+        forall(n in 1..N) % each non-self-parent node must have a chosen edge from its parent
+              (parent[n] != n -> exists(e in 1..E where to[e] = n)(es[e] /\ from[e] = parent[n])) /\
+        % nodes connected by chosen edges must be chosen
+        subgraph(N,E,from,to,ns,es);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_dreachable_multiroot_int_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_dreachable_multiroot_reif(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                        array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es,
+                                        var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_enum.mzn

@@ -0,0 +1,15 @@
+include "subgraph.mzn";
+
+predicate fzn_reachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                  array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    let {
+        int: E = length(es);
+        set of int: NODE = index_set(ns);
+        array[1..2*E] of NODE: dfrom   = from ++ to;
+        array[1..2*E] of NODE: dto     = to ++ from;
+        array[1..2*E] of var bool: des = es ++ es;
+    } in
+        /* duplicate the edges so that we can use directed graph reachability */
+        fzn_dreachable_multiroot(dfrom,dto,rs,ns,des);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_enum_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_reachable_multiroot_reif(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                                       array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es,
+                                       var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_int.mzn

@@ -0,0 +1,13 @@
+include "subgraph.mzn";
+
+predicate fzn_reachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                  array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    let {
+        array[1..2*E] of 1..N: dfrom   = from ++ to;
+        array[1..2*E] of 1..N: dto     = to ++ from;
+        array[1..2*E] of var bool: des = es ++ es;
+    } in
+        /* duplicate the edges so that we can use directed graph reachability */
+        fzn_dreachable_multiroot(N,2*E,dfrom,dto,rs,ns,des);
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/fzn_reachable_multiroot_int_reif.mzn

@@ -0,0 +1,6 @@
+predicate fzn_reachable_multiroot_reif(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                                       array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es,
+                                       var bool: b) =
+  abort("Reified dreachable_multiroot constraint is not supported");
+
+%-----------------------------------------------------------------------------%

share/minizinc/std/globals.mzn

@@ -64,6 +64,7 @@ include "bin_packing_load_fn.mzn";
 include "bounded_path.mzn";
 include "circuit.mzn";
 include "circuit_opt.mzn";
+include "cluster.mzn";
 include "connected.mzn";
 include "cost_mdd.mzn";
 include "cost_regular.mzn";
@@ -129,6 +130,7 @@ include "piecewise_linear_non_continuous.mzn";
 include "range.mzn";
 include "range_fn.mzn";
 include "reachable.mzn";
+include "reachable_multiroot.mzn";
 include "regular.mzn";
 include "regular_nfa.mzn";
 include "regular_regexp.mzn";

share/minizinc/std/reachable_multiroot.mzn

@@ -0,0 +1,100 @@
+include "fzn_reachable_multiroot_int.mzn";
+include "fzn_reachable_multiroot_int_reif.mzn";
+include "fzn_reachable_multiroot_enum.mzn";
+include "fzn_reachable_multiroot_enum_reif.mzn";
+include "fzn_dreachable_multiroot_int.mzn";
+include "fzn_dreachable_multiroot_int_reif.mzn";
+include "fzn_dreachable_multiroot_enum.mzn";
+include "fzn_dreachable_multiroot_enum_reif.mzn";
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given directed graph to be reachable from roots \a rs.
+
+    @param N: the number of nodes in the given graph
+    @param E: the number of edges in the given graph
+    @param from: the leaving node 1..\a N for each edge
+    @param to: the entering node 1..\a N for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate dreachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                               array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    assert(index_set(from) = 1..E,"dreachable_multiroot: index set of from must be 1..\(E)") /\
+    assert(index_set(to) = 1..E,"dreachable_multiroot: index set of to must be 1..\(E)") /\
+    assert(index_set(rs) = 1..N,"dreachable_multiroot: index set of rs must be 1..\(N)") /\
+    assert(index_set(ns) = 1..N,"dreachable_multiroot: index set of ns must be 1..\(N)") /\
+    assert(index_set(es) = 1..E,"dreachable_multiroot: index set of es must be 1..\(E)") /\
+    fzn_dreachable_multiroot(N,E,from,to,rs,ns,es);
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given directed graph to be reachable from roots \a rs.
+
+    @param from: the leaving node for each edge
+    @param to: the entering node for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate dreachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                               array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    assert(index_set(from) = index_set(to),"dreachable_multiroot: index set of from and to must be identical") /\
+    assert(index_set(from) = index_set(es),"dreachable_multiroot: index set of from and es must be identical") /\
+    assert(dom_array(from) subset index_set(rs),"dreachable_multiroot: nodes in from must be in index set of rs") /\
+    assert(dom_array(to) subset index_set(rs),"dreachable_multiroot: nodes in to must be in index set of rs") /\
+    assert(dom_array(from) subset index_set(ns),"dreachable_multiroot: nodes in from must be in index set of ns") /\
+    assert(dom_array(to) subset index_set(ns),"dreachable_multiroot: nodes in to must be in index set of ns") /\
+    fzn_dreachable_multiroot(
+        index2int(enum2int(from)),
+        index2int(enum2int(to)),
+        index2int(rs),
+        index2int(ns),
+        index2int(es)
+    );
+
+%-----------------------------------------------------------------------------%
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given undirected graph to be reachable from roots \a rs.
+
+    @param N: the number of nodes in the given graph
+    @param E: the number of edges in the given graph
+    @param from: the leaving node 1..\a N for each edge
+    @param to: the entering node 1..\a N for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate reachable_multiroot(int: N, int: E, array[int] of int: from, array[int] of int: to,
+                              array[int] of var bool: rs, array[int] of var bool: ns, array[int] of var bool: es) =
+    assert(index_set(from) = 1..E,"reachable_multiroot: index set of from must be 1..\(E)") /\
+    assert(index_set(to) = 1..E,"reachable_multiroot: index set of to must be 1..\(E)") /\
+    assert(index_set(rs) = 1..N,"reachable_multiroot: index set of rs must be 1..\(N)") /\
+    assert(index_set(ns) = 1..N,"reachable_multiroot: index set of ns must be 1..\(N)") /\
+    assert(index_set(es) = 1..E,"reachable_multiroot: index set of es must be 1..\(E)") /\
+    fzn_reachable_multiroot(N,E,from,to,rs,ns,es);
+
+/** @group globals.graph
+    Constrains the subgraph \a ns and \a es of a given undirected graph to be reachable from roots \a rs.
+
+    @param from: the leaving node for each edge
+    @param to: the entering node for each edge
+    @param rs: a Boolean for each node whether it is a root node (which may be variable)
+    @param ns: a Boolean for each node whether it is in the subgraph
+    @param es: a Boolean for each edge whether it is in the subgraph
+*/
+predicate reachable_multiroot(array[$$E] of $$N: from, array[$$E] of $$N: to,
+                              array[$$N] of var bool: rs, array[$$N] of var bool: ns, array[$$E] of var bool: es) =
+    assert(index_set(from) = index_set(to),"reachable_multiroot: index set of from and to must be identical") /\
+    assert(index_set(from) = index_set(es),"reachable_multiroot: index set of from and es must be identical") /\
+    assert(dom_array(from) subset index_set(rs),"reachable_multiroot: nodes in from must be in index set of rs") /\
+    assert(dom_array(to) subset index_set(rs),"reachable_multiroot: nodes in to must be in index set of rs") /\
+    assert(dom_array(from) subset index_set(ns),"reachable_multiroot: nodes in from must be in index set of ns") /\
+    assert(dom_array(to) subset index_set(ns),"reachable_multiroot: nodes in to must be in index set of ns") /\
+    fzn_reachable_multiroot(
+        index2int(enum2int(from)),
+        index2int(enum2int(to)),
+        index2int(rs),
+        index2int(ns),
+        index2int(es)
+    );